We present a hierarchical framework for analysing propositional linear-timetemporal logic (PTL) to obtain standard results such as a small model property,decision procedures and axiomatic completeness. Both finite time and infinitetime are considered and one consequent benefit of the framework is the abilityto systematically reduce infinite-time reasoning to finite-time reasoning. Thetreatment of PTL with both the operator Until and past time naturally reducesto that for PTL without either one. Our method utilises a low-level normal formfor PTL called a "transition configuration". In addition, we employ reasoningabout intervals of time. Besides being hierarchical and interval-based, theapproach differs from other analyses of PTL typically based on sets of formulasand sequences of such sets. Instead we describe models using time intervalsrepresented as finite and infinite sequences of states. The analysis relateslarger intervals with smaller ones. Steps involved are expressed inPropositional Interval Temporal Logic (PITL) which is better suited than PTLfor sequentially combining and decomposing formulas. Consequently, we canarticulate issues in PTL model construction of equal relevance in moreconventional analyses but normally only considered at the metalevel. We alsodescribe a decision procedure based on Binary Decision Diagrams.
展开▼
